(in-package "ACL2")

(defun sum-list (x)
        (declare (xargs :guard (integer-listp x)
                        :verify-guards nil))
        (cond ((endp x) 0)
              (t (+ (car x) (sum-list (cdr x))))))

(defthm sum-list-when-not-consp
  (implies (not (consp x))
           (equal (sum-list x)
                  0))
  :hints(("Goal" :in-theory (enable sum-list))))

(defthm sum-list-of-cons
  (equal (sum-list (cons a x))
         (+ a (sum-list x)))
  :hints(("Goal" :in-theory (enable sum-list))))

(defthm integerp-of-sum-list-when-integer-listp
  (implies (integer-listp x)
           (and (integerp (sum-list x))
                (<= 0 (sum-list x))))
  :hints(("Goal" :induct (len x))))

(defthm integerp-of-sum-list-when-integer-listp-linear
  (implies (integer-listp x)
           (<= 0 (sum-list x)))
  :rule-classes :linear)